\begin{tabbing}
R{-}sub\=\{i:l\}\+
\\[0ex]($A$; $B$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=if\= Rnone?($A$)\+\+
\\[0ex]then True
\-\\[0ex]if\= Rplus?($A$)\+
\\[0ex]then R{-}sub\{i:l\}(Rplus{-}left($A$); $B$) $\wedge$ R{-}sub\{i:l\}(Rplus{-}right($A$); $B$)
\-\\[0ex]if\= Rplus?($B$)\+
\\[0ex]then R{-}sub\{i:l\}($A$; Rplus{-}left($B$)) $\vee$ R{-}sub\{i:l\}($A$; Rplus{-}right($B$))
\-\\[0ex]else $A$ = $B$
\\[0ex]fi 
\\[0ex]
\-\\[0ex]{\em clarification:}
\\[0ex]
\\[0ex]R{-}sub\=\{i:l\}\+
\\[0ex]($A$; $B$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=if\= Rnone?($A$)\+\+
\\[0ex]then True
\-\\[0ex]if\= Rplus?($A$)\+
\\[0ex]then R{-}sub\{i:l\}(Rplus{-}left($A$); $B$) $\wedge$ R{-}sub\{i:l\}(Rplus{-}right($A$); $B$)
\-\\[0ex]if\= Rplus?($B$)\+
\\[0ex]then R{-}sub\{i:l\}($A$; Rplus{-}left($B$)) $\vee$ R{-}sub\{i:l\}($A$; Rplus{-}right($B$))
\-\\[0ex]else $A$ = $B$ $\in$ es\_realizer\{i:l\}
\\[0ex]fi 
\-\\[0ex]\emph{(recursive)}
\end{tabbing}